Search results for "Monadic predicate calculus"
showing 5 items of 5 documents
Monadic second-order logic over pictures and recognizability by tiling systems
1994
We show that a set of pictures (rectangular arrays of symbols) is recognized by a finite tiling system if and only if it is definable in existential monadic second-order logic. As a consequence, finite tiling systems constitute a notion of recognizability over two-dimensional inputs which at the same time generalizes finite-state recognizability over strings and matches a natural logic. The proof is based on the Ehrenfeucht-FraIsse technique for first-order logic and an implementation of “threshold counting” within tiling systems.
The Monadic Quantifier Alternation Hierarchy over Grids and Graphs
2002
AbstractThe monadic second-order quantifier alternation hierarchy over the class of finite graphs is shown to be strict. The proof is based on automata theoretic ideas and starts from a restricted class of graph-like structures, namely finite two-dimensional grids. Considering grids where the width is a function of the height, we prove that the difference between the levels k+1 and k of the monadic hierarchy is witnessed by a set of grids where this function is (k+1)-fold exponential. We then transfer the hierarchy result to the class of directed (or undirected) graphs, using an encoding technique called strong reduction. It is notable that one can obtain sets of graphs which occur arbitrar…
Local Normal Forms for First-Order Logic with Applications to Games and Automata
1999
Building on work of Gaifman [Gai82] it is shown that every first-order formula is logically equivalent to a formula of the form ∃ x_1,...,x_l, \forall y, φ where φ is r-local around y, i.e. quantification in φ is restricted to elements of the universe of distance at most r from y. \par From this and related normal forms, variants of the Ehrenfeucht game for first-order and existential monadic second-order logic are developed that restrict the possible strategies for the spoiler, one of the two players. This makes proofs of the existence of a winning strategy for the duplicator, the other player, easier and can thus simplify inexpressibility proofs. \par As another application, automata mode…
Monadic Second-Order Logic over Rectangular Pictures and Recognizability by Tiling Systems
1996
Abstract It is shown that a set of pictures (rectangular arrays of symbols) is recognized by a finite tiling system iff it is definable in existential monadic second-order logic. As a consequence, finite tiling systems constitute a notion of recognizability over two-dimensional inputs which at the same time generalizes finite-state recognizability over strings and also matches a natural logic. The proof is based on the Ehrenfeucht–Fraisse technique for first-order logic and an implementation of “threshold counting” within tiling systems.
The monadic quantifier alternation hierarchy over grids and pictures
1998
The subject of this paper is the expressive power of monadic second-order logic over two-dimensional grids. We give a new, self-contained game-theoretical proof of the nonexpressibility results of Matz and Thomas. As we show, this implies the strictness of the monadic second-order quantifier alternation hierarchy over grids.